(declare-fun a () Real)
(declare-fun b () Real)
(assert (not (= b 0)))
(check-sat)
(assert (> (/ 1 a) 0))
(assert (< b (- 1)))
(check-sat)
(declare-fun a () Real)
(declare-fun b () Real)
(assert (not (= b 0)))
(check-sat)
(assert (> (/ 1 a) 0))
(assert (< b (- 1)))
(check-sat)
